(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
insert(@x, @l) → insert#1(@x, @l, @x)
insert#1(tuple#2(@valX, @keyX), @l, @x) → insert#2(@l, @keyX, @valX, @x)
insert#2(::(@l1, @ls), @keyX, @valX, @x) → insert#3(@l1, @keyX, @ls, @valX, @x)
insert#2(nil, @keyX, @valX, @x) → ::(tuple#2(::(@valX, nil), @keyX), nil)
insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) → insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)
insert#4(#false, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(@vals1, @key1), insert(@x, @ls))
insert#4(#true, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(::(@valX, @vals1), @key1), @ls)
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(splitqs(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
sortAll(@l) → sortAll#1(@l)
sortAll#1(::(@x, @xs)) → sortAll#2(@x, @xs)
sortAll#1(nil) → nil
sortAll#2(tuple#2(@vals, @key), @xs) → ::(tuple#2(quicksort(@vals), @key), sortAll(@xs))
split(@l) → split#1(@l)
split#1(::(@x, @xs)) → insert(@x, split(@xs))
split#1(nil) → nil
splitAndSort(@l) → sortAll(split(@l))
splitqs(@pivot, @l) → splitqs#1(@l, @pivot)
splitqs#1(::(@x, @xs), @pivot) → splitqs#2(splitqs(@pivot, @xs), @pivot, @x)
splitqs#1(nil, @pivot) → tuple#2(nil, nil)
splitqs#2(tuple#2(@ls, @rs), @pivot, @x) → splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)
splitqs#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitqs#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
The (relative) TRS S consists of the following rules:
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
append(::(@x15111_5, @xs15112_5), @ys) →+ ::(@x15111_5, append(@xs15112_5, @ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs15112_5 / ::(@x15111_5, @xs15112_5)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)